\begin{tabbing}
$\forall$\=${\it es}$:ES, $Q_{1}$, $Q_{2}$, $R$:(E$\rightarrow$E$\rightarrow\mathbb{P}$), $A$, $B$:Type, ${\it Ia}_{1}$, ${\it Ia}_{2}$:AbsInterface($A$), ${\it Ib}_{1}$,\+
\\[0ex]${\it Ib}_{2}$:AbsInterface($B$), $f$:(E([${\it Ia}_{1}$?${\it Ia}_{2}$])$\rightarrow$$B$), $g_{1}$:(E(${\it Ib}_{1}$)$\rightarrow$E), $g_{2}$:(E(${\it Ib}_{2}$)$\rightarrow$E).
\-\\[0ex]${\it Ia}_{1}$ $\cap$ ${\it Ia}_{2}$ = 0
\\[0ex]$\Rightarrow$ ${\it Ib}_{1}$ $\cap$ ${\it Ib}_{2}$ = 0
\\[0ex]$\Rightarrow$ $g_{1}$ glues ${\it Ia}_{1}$:$Q_{1}$ $--$$f$$\rightarrow$ ${\it Ib}_{1}$:$R$
\\[0ex]$\Rightarrow$ $g_{2}$ glues ${\it Ia}_{2}$:$Q_{2}$ $--$$f$$\rightarrow$ ${\it Ib}_{2}$:$R$
\\[0ex]$\Rightarrow$ [\{${\it Ib}_{1}$\}? $g_{1}$ : $g_{2}$] glues [${\it Ia}_{1}$?${\it Ia}_{2}$]:$Q_{1}$$\mid$\{${\it Ia}_{1}$\} $\vee$ $Q_{2}$$\mid$\{${\it Ia}_{2}$\} $--$$f$$\rightarrow$ [${\it Ib}_{1}$?${\it Ib}_{2}$]:$R$
\end{tabbing}